$\forall$$T$:Type, $L$:$T$ List, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P$($i$) $\Rightarrow$ $i$$<$$j$ $\Rightarrow$ $P$($j$))
\\[0ex]$\Rightarrow$ ($\exists$$L_{1}$, $L_{2}$:$T$ List. $L$ $=$ ($L_{1}$ @ $L_{2}$) \& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P$($i$) $\Leftrightarrow$ $\parallel$$L_{1}$$\parallel\leq$$i$))